structure Systeml :> Systeml = struct

(* This is the WINDOWS implementation of the Systeml functionality.
   It is the very first thing compiled by the HOL build process so it
   absolutely can not depend on any other HOL source code. *)

structure Process = OS.Process
structure Path = OS.Path
structure FileSys = OS.FileSys

fun dquote s = concat ["\"", s, "\""]

fun concat_wspaces munge strl = String.concatWith " " (map munge strl)

fun systeml l = let
  val command = "call "^concat_wspaces dquote l
in
  Process.system command
end

fun systeml_out {outfile} c =
  Process.system
    ("call " ^ concat_wspaces dquote c ^ " > " ^ dquote outfile ^ " 2>&1")


(* would like to be using Posix.Process.exec, but this seems flakey on
   various machines (and is entirely unavailable on Moscow ML) *)
fun exec (comm, args) = OS.Process.exit (systeml (comm::tl args))

val protect = dquote

(* the _ps suffix stands for 'protected string', as opposed to the 'l'
   of systeml, which stands for 'list' of strings (all of which are
   presumed unprotected).  The problem is that on Windows, if you pass
   system a (protected) string such as
      "c:/program files/bar/baz" "arg1"
   then it has a fit.  It seems the only way of getting it to play nicely
   is to prefix the commandline with "call". *)
fun system_ps s = Process.system ("call " ^ s)

fun xable_string s = s^".exe"
fun mk_xable file =
    let val exe = file^".exe"
        val _ = FileSys.remove exe handle _ => ()
    in
      FileSys.rename{old=file, new=exe};
      OS.Process.success
    end

fun normPath s = Path.toString(Path.fromString s)

fun fullPath slist =
    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
                         (hd slist) (tl slist))

  fun get_first f [] = NONE
    | get_first f (h::t) = case f h of NONE => get_first f t
                                     | x => x


  fun find_my_path () = let
    (* assumes directory hasn't been changed yet *)
    val myname = CommandLine.name()
    val {dir,file} = Path.splitDirFile myname
  in
    if dir = "" then let
        val pathdirs = String.tokens (fn c => c = #";")
                                     (valOf (Process.getEnv "PATH"))
        open FileSys
        fun checkdir d = let
          val f = Path.concat(d,file)
        in
          if access(f, [A_READ, A_EXEC]) then SOME f else NONE
        end
      in
        valOf (get_first checkdir pathdirs)
      end
    else
      Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()}
  end


val HOLDIR = ""
val MOSMLDIR = ""
val OS = ""
val POLY = ""
val POLYC = ""
val POLY_VERSION = 0
val POLYMLLIBDIR = ""
val POLY_LDFLAGS = []
val POLY_LDFLAGS_STATIC = []
val CC = ""
val DEPDIR = ""
val GNUMAKE = ""
val DYNLIB = ""
val version = ""
val ML_SYSNAME = ""
val release = ""
val DOT_PATH = ""
val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]

val isUnix = false
local val cast : 'a -> int = Obj.magic
in
  fun pointer_eq (x:'a, y:'a) = (cast x = cast y)
end

val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"]
val build_log_file = fullPath [build_log_dir, "current-build-log"]
val make_log_file = "current-make-log"
val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"

local
  fun fopen file = (FileSys.remove file handle _ => (); TextIO.openOut file)
  fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
  fun q s = "\""^munge s^"\""
in
fun emit_hol_script target qend _ =
 let val ostrm = fopen(target^".bat")
     fun output s = TextIO.output(ostrm, s)
     val sigobj = q (fullPath [HOLDIR, "sigobj"])
     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
     val mosml = q (fullPath [MOSMLDIR, "mosml"])
 in
    output "@echo off\n";
    output "rem The bare HOL script\n";
    output "rem (automatically generated by HOL configuration)\n\n";
    output (String.concat["call ", mosml, " -P full -I ", sigobj, " ",
                          std_prelude, " %* ", q qend, "\n"]);
    TextIO.closeOut ostrm;
    target
 end


fun emit_hol_unquote_script target qend _ =
 let val ostrm = fopen(target^".bat")
     fun output s = TextIO.output(ostrm, s)
     val qfilter = q (fullPath [HOLDIR, "bin", "unquote"])
     val sigobj = q (fullPath [HOLDIR, "sigobj"])
     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
     val mosml = q (fullPath [MOSMLDIR, "mosml"])
     val qinit = q (fullPath [HOLDIR, "tools", "unquote-init.sml"])
 in
    output "@echo off\n";
    output "rem The HOL script (with quote preprocessing)\n";
    output "rem (automatically generated by HOL configuration)\n\n";
    output  (String.concat ["call ", qfilter, " | ", mosml,
                          " -P full -I ", sigobj, " ",
                            std_prelude, " ", qinit, " %* ",
                            q qend, "\n"]);
    TextIO.closeOut ostrm;
    target
 end
end (* local *)

fun quietbind s = ()
fun bindstr s = s

end; (* struct *)
